$\vdash$  $\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $f$:($\forall$$x$:$T$. Dec($P$($x$))), $x$:$T$. ($\uparrow$can{-}apply(p{-}co{-}filter($f$);$x$)) $\Leftarrow\!\Rightarrow$ ($\neg$$P$($x$))